The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
    ↳1 CpxTrsMatchBoundsTAProof (⇔, 9 ms)
    ↳2 BOUNDS(1, n^1)
    ↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
        ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳6 CdtProblem
        ↳7 CdtUsableRulesProof (⇔, 1 ms)
        ↳8 CdtProblem
        ↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 59 ms)
        ↳10 CdtProblem
        ↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 13 ms)
        ↳12 CdtProblem
        ↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳14 CdtProblem
        ↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳16 CdtProblem
        ↳17 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳18 CdtProblem
        ↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳20 CdtProblem
        ↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳22 CdtProblem
        ↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳24 CdtProblem
        ↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳26 CdtProblem
        ↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳28 CdtProblem
        ↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳30 CdtProblem
        ↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳32 CdtProblem
        ↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳34 CdtProblem
        ↳35 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳36 CdtProblem
        ↳37 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳38 CdtProblem
        ↳39 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳40 CdtProblem
        ↳41 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 7577 ms)
        ↳42 CdtProblem
        ↳43 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 7594 ms)
        ↳44 CdtProblem
        ↳45 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 7667 ms)
        ↳46 CdtProblem
        ↳47 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳48 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
nil0() → 0
.0(0, 0) → 0
f0(0) → 1
g0(0) → 2
nil1() → 1
nil1() → 3
f1(0) → 4
.1(3, 4) → 1
.1(0, 0) → 6
.1(0, 6) → 5
f1(5) → 1
nil1() → 2
g1(0) → 7
nil1() → 8
.1(7, 8) → 2
.1(0, 0) → 10
.1(10, 0) → 9
g1(9) → 2
nil1() → 4
.1(3, 4) → 4
f1(6) → 4
f1(5) → 4
.1(0, 6) → 6
nil1() → 7
.1(7, 8) → 7
g1(10) → 7
g1(9) → 7
.1(10, 0) → 10

(2) BOUNDS(1, n^1)

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(nil) → c
F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(nil) → c3
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(nil) → c
F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(nil) → c3
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c, c1, c2, c3, c4, c5

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

G(nil) → c3
F(nil) → c

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

f(nil) → nil
f(.(nil, z0)) → .(nil, f(z0))
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2)))
g(nil) → nil
g(.(z0, nil)) → .(g(z0), nil)
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(.(z0, nil)) → c4(G(z0))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = [2] + x1 + x2   
POL(F(x1)) = 0   
POL(G(x1)) = [2]x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(nil) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

G(.(z0, nil)) → c4(G(z0))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(nil, z0)) → c1(F(z0))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x1, x2)) = x1 + x2   
POL(F(x1)) = x1   
POL(G(x1)) = 0   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(nil) = [1]   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, z0)) → c1(F(z0))
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

G(.(z0, nil)) → c4(G(z0))
F(.(nil, z0)) → c1(F(z0))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, z0)) → c1(F(z0)) by

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
S tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2))))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

G(.(z0, nil)) → c4(G(z0))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) by

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

G(.(z0, nil)) → c4(G(z0))
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
S tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
K tuples:

G(.(z0, nil)) → c4(G(z0))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
Defined Rule Symbols:none

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, nil)) → c4(G(z0)) by

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
S tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
K tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
Defined Rule Symbols:none

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) by

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0)))
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) by

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) by

F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2))))
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) by

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
S tuples:

F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2))))
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) by

F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
S tuples:

F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) by

F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil)))
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:none

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) by

G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
Defined Rule Symbols:none

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) by

G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2))))
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:none

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) by

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
S tuples:

G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil)))
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:none

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) by

G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
S tuples:

G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:none

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

(39) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) by

G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(41) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]:
Non-tuple symbols:
M( .(x1, x2) ) =
/0\
\0/
+
/10\
\00/
·x1+
/14\
\00/
·x2

M( nil ) =
/0\
\2/

Tuple symbols:
M( G(x1) ) =
/0\
\0/
+
/00\
\00/
·x1

M( c1(x1) ) =
/0\
\0/
+
/10\
\00/
·x1

M( c5(x1) ) =
/0\
\0/
+
/14\
\00/
·x1

M( c4(x1) ) =
/0\
\0/
+
/10\
\00/
·x1

M( F(x1) ) =
/0\
\0/
+
/10\
\00/
·x1

M( c2(x1) ) =
/0\
\0/
+
/10\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(43) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]:
Non-tuple symbols:
M( .(x1, x2) ) =
/0\
\2/
+
/04\
\01/
·x1+
/10\
\01/
·x2

M( nil ) =
/0\
\2/

Tuple symbols:
M( G(x1) ) =
/0\
\4/
+
/00\
\00/
·x1

M( c1(x1) ) =
/4\
\2/
+
/12\
\00/
·x1

M( c5(x1) ) =
/0\
\0/
+
/10\
\01/
·x1

M( c4(x1) ) =
/0\
\3/
+
/10\
\00/
·x1

M( F(x1) ) =
/4\
\2/
+
/14\
\00/
·x1

M( c2(x1) ) =
/4\
\2/
+
/11\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(45) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]:
Non-tuple symbols:
M( .(x1, x2) ) =
/2\
\2/
+
/10\
\01/
·x1+
/14\
\00/
·x2

M( nil ) =
/0\
\0/

Tuple symbols:
M( G(x1) ) =
/2\
\0/
+
/10\
\00/
·x1

M( c1(x1) ) =
/0\
\3/
+
/10\
\00/
·x1

M( c5(x1) ) =
/2\
\0/
+
/10\
\00/
·x1

M( c4(x1) ) =
/2\
\0/
+
/14\
\00/
·x1

M( F(x1) ) =
/0\
\4/
+
/00\
\00/
·x1

M( c2(x1) ) =
/0\
\4/
+
/10\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:none
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0))))
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2)))
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2)))
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil)))
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3)))))
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil))))
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0)))))
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3))))
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3))))
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2))))
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2))))
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3)))))
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil))))
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil)))
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil)))
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil)))
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
Defined Rule Symbols:none

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

(47) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(48) BOUNDS(1, 1)